YES 9.449 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ IFR

mainModule List
  ((delete :: Ratio Int  ->  [Ratio Int ->  [Ratio Int]) :: Ratio Int  ->  [Ratio Int ->  [Ratio Int])

module List where
  import qualified Maybe
import qualified Prelude

  delete :: Eq a => a  ->  [a ->  [a]
delete deleteBy (==)

  deleteBy :: (a  ->  a  ->  Bool ->  a  ->  [a ->  [a]
deleteBy _ _ [] []
deleteBy eq x (y : ys if x `eq` y then ys else y : deleteBy eq x ys


module Maybe where
  import qualified List
import qualified Prelude



If Reductions:
The following If expression
if eq x y then ys else y : deleteBy eq x ys

is transformed to
deleteBy0 ys y eq x True = ys
deleteBy0 ys y eq x False = y : deleteBy eq x ys



↳ HASKELL
  ↳ IFR
HASKELL
      ↳ BR

mainModule List
  ((delete :: Ratio Int  ->  [Ratio Int ->  [Ratio Int]) :: Ratio Int  ->  [Ratio Int ->  [Ratio Int])

module List where
  import qualified Maybe
import qualified Prelude

  delete :: Eq a => a  ->  [a ->  [a]
delete deleteBy (==)

  deleteBy :: (a  ->  a  ->  Bool ->  a  ->  [a ->  [a]
deleteBy _ _ [] []
deleteBy eq x (y : ysdeleteBy0 ys y eq x (x `eq` y)

  
deleteBy0 ys y eq x True ys
deleteBy0 ys y eq x False y : deleteBy eq x ys


module Maybe where
  import qualified List
import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
HASKELL
          ↳ COR

mainModule List
  ((delete :: Ratio Int  ->  [Ratio Int ->  [Ratio Int]) :: Ratio Int  ->  [Ratio Int ->  [Ratio Int])

module List where
  import qualified Maybe
import qualified Prelude

  delete :: Eq a => a  ->  [a ->  [a]
delete deleteBy (==)

  deleteBy :: (a  ->  a  ->  Bool ->  a  ->  [a ->  [a]
deleteBy vw vx [] []
deleteBy eq x (y : ysdeleteBy0 ys y eq x (x `eq` y)

  
deleteBy0 ys y eq x True ys
deleteBy0 ys y eq x False y : deleteBy eq x ys


module Maybe where
  import qualified List
import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
HASKELL
              ↳ Narrow

mainModule List
  (delete :: Ratio Int  ->  [Ratio Int ->  [Ratio Int])

module List where
  import qualified Maybe
import qualified Prelude

  delete :: Eq a => a  ->  [a ->  [a]
delete deleteBy (==)

  deleteBy :: (a  ->  a  ->  Bool ->  a  ->  [a ->  [a]
deleteBy vw vx [] []
deleteBy eq x (y : ysdeleteBy0 ys y eq x (x `eq` y)

  
deleteBy0 ys y eq x True ys
deleteBy0 ys y eq x False y : deleteBy eq x ys


module Maybe where
  import qualified List
import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
QDP
                  ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

new_deleteBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Zero), Neg(Succ(ww40100))), ww41)) → new_deleteBy05(ww41, ww40100, ww3100, ww3100, ww40100)
new_deleteBy08(ww227, ww228, Pos(Succ(ww22900)), ww230, Neg(Zero), Zero, Zero) → new_deleteBy019(ww227, ww228, Pos(Succ(ww22900)), ww230, Neg(Zero))
new_deleteBy08(ww227, ww228, Neg(Succ(ww22900)), ww230, Pos(Zero), Zero, Zero) → new_deleteBy019(ww227, ww228, Neg(Succ(ww22900)), ww230, Pos(Zero))
new_deleteBy011(ww334, ww335, ww336, Succ(ww3370), Zero) → new_deleteBy(:%(Neg(Zero), Pos(Succ(ww336))), ww334)
new_deleteBy04(ww298, ww299, ww300, Succ(ww3010), Succ(ww3020)) → new_deleteBy04(ww298, ww299, ww300, ww3010, ww3020)
new_deleteBy0(ww219, ww220, Neg(Zero), ww222, Neg(Succ(ww22300)), Zero, Zero) → new_deleteBy02(ww219, ww220, Neg(Zero), ww222, Neg(Succ(ww22300)))
new_deleteBy0(ww219, ww220, Neg(ww2210), ww222, Pos(Succ(ww22300)), Zero, Zero) → new_deleteBy02(ww219, ww220, Neg(ww2210), ww222, Pos(Succ(ww22300)))
new_deleteBy0(ww219, ww220, Pos(ww2210), ww222, Neg(Succ(ww22300)), Zero, Zero) → new_deleteBy02(ww219, ww220, Pos(ww2210), ww222, Neg(Succ(ww22300)))
new_deleteBy024(ww340, ww341, ww342) → new_deleteBy(:%(Neg(Zero), Neg(Succ(ww342))), ww340)
new_deleteBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Zero), Pos(Succ(ww40100))), ww41)) → new_deleteBy011(ww41, ww40100, ww3100, ww3100, ww40100)
new_deleteBy05(ww304, ww305, ww306, Zero, Succ(ww3080)) → new_deleteBy014(ww304, ww305, ww306)
new_deleteBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Zero), Pos(ww4010)), ww41)) → new_deleteBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_deleteBy00(ww219, ww220, ww221, ww222, ww223) → new_deleteBy(:%(Pos(Succ(ww222)), ww223), ww219)
new_deleteBy09(ww322, ww323, ww324, Succ(ww3250), Zero) → new_deleteBy(:%(Neg(Zero), Pos(Succ(ww324))), ww322)
new_deleteBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Pos(Zero), Pos(Succ(ww40100))), ww41)) → new_deleteBy04(ww41, ww40100, ww3100, ww3100, ww40100)
new_deleteBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Neg(Zero), Neg(Zero)), ww41)) → new_deleteBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_deleteBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Zero), Neg(Succ(ww40100))), ww41)) → new_deleteBy010(ww41, ww40100, ww3100, ww3100, ww40100)
new_deleteBy014(ww304, ww305, ww306) → new_deleteBy(:%(Pos(Zero), Neg(Succ(ww306))), ww304)
new_deleteBy(:%(Neg(Zero), Pos(Zero)), :(:%(Pos(Zero), Neg(Succ(ww40100))), ww41)) → new_deleteBy(:%(Neg(Zero), Pos(Zero)), ww41)
new_deleteBy(:%(Neg(Zero), ww31), :(:%(Pos(Succ(ww40000)), ww401), ww41)) → new_deleteBy(:%(Neg(Zero), ww31), ww41)
new_deleteBy(:%(Pos(Zero), Neg(Zero)), :(:%(Neg(Zero), Pos(Succ(ww40100))), ww41)) → new_deleteBy(:%(Pos(Zero), Neg(Zero)), ww41)
new_deleteBy(:%(Pos(Zero), Neg(Zero)), :(:%(Pos(Zero), Neg(Succ(ww40100))), ww41)) → new_deleteBy(:%(Pos(Zero), Neg(Zero)), ww41)
new_deleteBy(:%(Neg(Zero), Pos(Zero)), :(:%(Neg(Zero), Pos(Succ(ww40100))), ww41)) → new_deleteBy(:%(Neg(Zero), Pos(Zero)), ww41)
new_deleteBy08(ww227, ww228, ww229, ww230, ww231, Succ(ww2320), Succ(ww2330)) → new_deleteBy08(ww227, ww228, ww229, ww230, ww231, ww2320, ww2330)
new_deleteBy08(ww227, ww228, Pos(Succ(ww22900)), ww230, Pos(Zero), Zero, Zero) → new_deleteBy019(ww227, ww228, Pos(Succ(ww22900)), ww230, Pos(Zero))
new_deleteBy(:%(Pos(Succ(ww3000)), ww31), :(:%(Pos(Succ(ww40000)), ww401), ww41)) → new_deleteBy0(ww41, ww40000, ww401, ww3000, ww31, ww3000, ww40000)
new_deleteBy01(ww412, ww413, ww414, ww415, ww416, Succ(ww4170), Zero) → new_deleteBy02(ww412, ww413, Pos(Succ(ww414)), ww415, Pos(Succ(ww416)))
new_deleteBy01(ww412, ww413, ww414, ww415, ww416, Zero, Succ(ww4180)) → new_deleteBy02(ww412, ww413, Pos(Succ(ww414)), ww415, Pos(Succ(ww416)))
new_deleteBy(:%(Pos(Zero), Neg(Zero)), :(:%(Pos(Zero), Pos(Succ(ww40100))), ww41)) → new_deleteBy(:%(Pos(Zero), Neg(Zero)), ww41)
new_deleteBy(:%(Neg(Zero), Pos(Zero)), :(:%(Pos(Zero), Pos(Succ(ww40100))), ww41)) → new_deleteBy(:%(Neg(Zero), Pos(Zero)), ww41)
new_deleteBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Pos(Zero), Neg(ww4010)), ww41)) → new_deleteBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_deleteBy02(ww219, ww220, ww221, ww222, ww223) → new_deleteBy(:%(Pos(Succ(ww222)), ww223), ww219)
new_deleteBy(:%(Neg(Succ(ww3000)), ww31), :(:%(Neg(Succ(ww40000)), ww401), ww41)) → new_deleteBy08(ww41, ww40000, ww401, ww3000, ww31, ww3000, ww40000)
new_deleteBy07(ww316, ww317, ww318, Zero, Succ(ww3200)) → new_deleteBy016(ww316, ww317, ww318)
new_deleteBy06(ww310, ww311, ww312, Zero, Succ(ww3140)) → new_deleteBy015(ww310, ww311, ww312)
new_deleteBy012(ww340, ww341, ww342, Zero, Succ(ww3440)) → new_deleteBy024(ww340, ww341, ww342)
new_deleteBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Zero), Pos(ww4010)), ww41)) → new_deleteBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_deleteBy0(ww219, ww220, ww221, ww222, ww223, Succ(ww2240), Zero) → new_deleteBy(:%(Pos(Succ(ww222)), ww223), ww219)
new_deleteBy013(ww298, ww299, ww300) → new_deleteBy(:%(Pos(Zero), Pos(Succ(ww300))), ww298)
new_deleteBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Neg(Zero), Pos(ww4010)), ww41)) → new_deleteBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_deleteBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Pos(Zero), Neg(ww4010)), ww41)) → new_deleteBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_deleteBy(:%(Neg(Zero), Neg(Zero)), :(:%(Neg(Zero), Pos(Succ(ww40100))), ww41)) → new_deleteBy(:%(Neg(Zero), Neg(Zero)), ww41)
new_deleteBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Zero), Neg(ww4010)), ww41)) → new_deleteBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_deleteBy(:%(Neg(Zero), Neg(Zero)), :(:%(Pos(Zero), Neg(Succ(ww40100))), ww41)) → new_deleteBy(:%(Neg(Zero), Neg(Zero)), ww41)
new_deleteBy020(ww436, ww437, ww438, ww439, ww440, Succ(ww4410), Succ(ww4420)) → new_deleteBy020(ww436, ww437, ww438, ww439, ww440, ww4410, ww4420)
new_deleteBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Neg(Zero), Neg(Succ(ww40100))), ww41)) → new_deleteBy012(ww41, ww40100, ww3100, ww3100, ww40100)
new_deleteBy(:%(Pos(Succ(ww3000)), ww31), :(:%(Neg(ww4000), ww401), ww41)) → new_deleteBy(:%(Pos(Succ(ww3000)), ww31), ww41)
new_deleteBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Zero), Pos(Zero)), ww41)) → new_deleteBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_deleteBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Zero), Neg(Zero)), ww41)) → new_deleteBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_deleteBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Neg(Zero), Pos(ww4010)), ww41)) → new_deleteBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_deleteBy08(ww227, ww228, Neg(Succ(ww22900)), ww230, Neg(Zero), Zero, Zero) → new_deleteBy019(ww227, ww228, Neg(Succ(ww22900)), ww230, Neg(Zero))
new_deleteBy07(ww316, ww317, ww318, Succ(ww3190), Zero) → new_deleteBy(:%(Pos(Zero), Neg(Succ(ww318))), ww316)
new_deleteBy08(ww227, ww228, Neg(Zero), ww230, Neg(Succ(ww23100)), Zero, Zero) → new_deleteBy019(ww227, ww228, Neg(Zero), ww230, Neg(Succ(ww23100)))
new_deleteBy021(ww322, ww323, ww324) → new_deleteBy(:%(Neg(Zero), Pos(Succ(ww324))), ww322)
new_deleteBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Neg(Zero), Neg(Succ(ww40100))), ww41)) → new_deleteBy07(ww41, ww40100, ww3100, ww3100, ww40100)
new_deleteBy(:%(Neg(Zero), Neg(Zero)), :(:%(Neg(Zero), Neg(Succ(ww40100))), ww41)) → new_deleteBy(:%(Neg(Zero), Neg(Zero)), ww41)
new_deleteBy0(ww219, ww220, Pos(Succ(ww22100)), ww222, Pos(Zero), Zero, Zero) → new_deleteBy02(ww219, ww220, Pos(Succ(ww22100)), ww222, Pos(Zero))
new_deleteBy07(ww316, ww317, ww318, Succ(ww3190), Succ(ww3200)) → new_deleteBy07(ww316, ww317, ww318, ww3190, ww3200)
new_deleteBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Neg(Zero), Neg(Zero)), ww41)) → new_deleteBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_deleteBy08(ww227, ww228, ww229, ww230, ww231, Succ(ww2320), Zero) → new_deleteBy(:%(Neg(Succ(ww230)), ww231), ww227)
new_deleteBy022(ww328, ww329, ww330) → new_deleteBy(:%(Neg(Zero), Neg(Succ(ww330))), ww328)
new_deleteBy010(ww328, ww329, ww330, Succ(ww3310), Zero) → new_deleteBy(:%(Neg(Zero), Neg(Succ(ww330))), ww328)
new_deleteBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Zero), Neg(ww4010)), ww41)) → new_deleteBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_deleteBy015(ww310, ww311, ww312) → new_deleteBy(:%(Pos(Zero), Pos(Succ(ww312))), ww310)
new_deleteBy023(ww334, ww335, ww336) → new_deleteBy(:%(Neg(Zero), Pos(Succ(ww336))), ww334)
new_deleteBy010(ww328, ww329, ww330, Succ(ww3310), Succ(ww3320)) → new_deleteBy010(ww328, ww329, ww330, ww3310, ww3320)
new_deleteBy03(ww420, ww421, ww422, ww423, ww424, Succ(ww4250), Succ(ww4260)) → new_deleteBy03(ww420, ww421, ww422, ww423, ww424, ww4250, ww4260)
new_deleteBy01(ww412, ww413, ww414, ww415, ww416, Succ(ww4170), Succ(ww4180)) → new_deleteBy01(ww412, ww413, ww414, ww415, ww416, ww4170, ww4180)
new_deleteBy09(ww322, ww323, ww324, Zero, Succ(ww3260)) → new_deleteBy021(ww322, ww323, ww324)
new_deleteBy(:%(Neg(Succ(ww3000)), ww31), :(:%(Neg(Zero), ww401), ww41)) → new_deleteBy(:%(Neg(Succ(ww3000)), ww31), ww41)
new_deleteBy018(ww428, ww429, ww430, ww431, ww432, Zero, Succ(ww4340)) → new_deleteBy019(ww428, ww429, Pos(Succ(ww430)), ww431, Pos(Succ(ww432)))
new_deleteBy018(ww428, ww429, ww430, ww431, ww432, Succ(ww4330), Zero) → new_deleteBy019(ww428, ww429, Pos(Succ(ww430)), ww431, Pos(Succ(ww432)))
new_deleteBy010(ww328, ww329, ww330, Zero, Succ(ww3320)) → new_deleteBy022(ww328, ww329, ww330)
new_deleteBy05(ww304, ww305, ww306, Succ(ww3070), Zero) → new_deleteBy(:%(Pos(Zero), Neg(Succ(ww306))), ww304)
new_deleteBy017(ww227, ww228, ww229, ww230, ww231) → new_deleteBy(:%(Neg(Succ(ww230)), ww231), ww227)
new_deleteBy011(ww334, ww335, ww336, Zero, Succ(ww3380)) → new_deleteBy023(ww334, ww335, ww336)
new_deleteBy0(ww219, ww220, Pos(Zero), ww222, Pos(Succ(ww22300)), Zero, Zero) → new_deleteBy02(ww219, ww220, Pos(Zero), ww222, Pos(Succ(ww22300)))
new_deleteBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Zero), Neg(Zero)), ww41)) → new_deleteBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_deleteBy0(ww219, ww220, Pos(Succ(ww22100)), ww222, Pos(Succ(ww22300)), Zero, Zero) → new_deleteBy01(ww219, ww220, ww22100, ww222, ww22300, ww22300, ww22100)
new_deleteBy(:%(Pos(Zero), Pos(Zero)), :(:%(Neg(Zero), Neg(Succ(ww40100))), ww41)) → new_deleteBy(:%(Pos(Zero), Pos(Zero)), ww41)
new_deleteBy04(ww298, ww299, ww300, Succ(ww3010), Zero) → new_deleteBy(:%(Pos(Zero), Pos(Succ(ww300))), ww298)
new_deleteBy06(ww310, ww311, ww312, Succ(ww3130), Succ(ww3140)) → new_deleteBy06(ww310, ww311, ww312, ww3130, ww3140)
new_deleteBy(:%(Pos(Zero), Pos(Zero)), :(:%(Neg(Zero), Pos(Succ(ww40100))), ww41)) → new_deleteBy(:%(Pos(Zero), Pos(Zero)), ww41)
new_deleteBy(:%(Pos(Zero), Pos(Zero)), :(:%(Pos(Zero), Neg(Succ(ww40100))), ww41)) → new_deleteBy(:%(Pos(Zero), Pos(Zero)), ww41)
new_deleteBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Pos(Zero), Pos(Zero)), ww41)) → new_deleteBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_deleteBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Pos(Zero), Pos(Zero)), ww41)) → new_deleteBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_deleteBy08(ww227, ww228, ww229, ww230, ww231, Zero, Succ(ww2330)) → new_deleteBy017(ww227, ww228, ww229, ww230, ww231)
new_deleteBy(:%(Pos(Zero), ww31), :(:%(Neg(Succ(ww40000)), ww401), ww41)) → new_deleteBy(:%(Pos(Zero), ww31), ww41)
new_deleteBy018(ww428, ww429, ww430, ww431, ww432, Succ(ww4330), Succ(ww4340)) → new_deleteBy018(ww428, ww429, ww430, ww431, ww432, ww4330, ww4340)
new_deleteBy08(ww227, ww228, Neg(ww2290), ww230, Pos(Succ(ww23100)), Zero, Zero) → new_deleteBy019(ww227, ww228, Neg(ww2290), ww230, Pos(Succ(ww23100)))
new_deleteBy08(ww227, ww228, Pos(ww2290), ww230, Neg(Succ(ww23100)), Zero, Zero) → new_deleteBy019(ww227, ww228, Pos(ww2290), ww230, Neg(Succ(ww23100)))
new_deleteBy(:%(Neg(Succ(ww3000)), ww31), :(:%(Pos(ww4000), ww401), ww41)) → new_deleteBy(:%(Neg(Succ(ww3000)), ww31), ww41)
new_deleteBy012(ww340, ww341, ww342, Succ(ww3430), Zero) → new_deleteBy(:%(Neg(Zero), Neg(Succ(ww342))), ww340)
new_deleteBy09(ww322, ww323, ww324, Succ(ww3250), Succ(ww3260)) → new_deleteBy09(ww322, ww323, ww324, ww3250, ww3260)
new_deleteBy0(ww219, ww220, Neg(Succ(ww22100)), ww222, Neg(Zero), Zero, Zero) → new_deleteBy02(ww219, ww220, Neg(Succ(ww22100)), ww222, Neg(Zero))
new_deleteBy016(ww316, ww317, ww318) → new_deleteBy(:%(Pos(Zero), Neg(Succ(ww318))), ww316)
new_deleteBy012(ww340, ww341, ww342, Succ(ww3430), Succ(ww3440)) → new_deleteBy012(ww340, ww341, ww342, ww3430, ww3440)
new_deleteBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Zero), Pos(Succ(ww40100))), ww41)) → new_deleteBy06(ww41, ww40100, ww3100, ww3100, ww40100)
new_deleteBy020(ww436, ww437, ww438, ww439, ww440, Succ(ww4410), Zero) → new_deleteBy019(ww436, ww437, Neg(Succ(ww438)), ww439, Neg(Succ(ww440)))
new_deleteBy020(ww436, ww437, ww438, ww439, ww440, Zero, Succ(ww4420)) → new_deleteBy019(ww436, ww437, Neg(Succ(ww438)), ww439, Neg(Succ(ww440)))
new_deleteBy(:%(Pos(Zero), Pos(Zero)), :(:%(Pos(Zero), Pos(Succ(ww40100))), ww41)) → new_deleteBy(:%(Pos(Zero), Pos(Zero)), ww41)
new_deleteBy(:%(Neg(Zero), ww31), :(:%(Neg(Succ(ww40000)), ww401), ww41)) → new_deleteBy(:%(Neg(Zero), ww31), ww41)
new_deleteBy0(ww219, ww220, ww221, ww222, ww223, Succ(ww2240), Succ(ww2250)) → new_deleteBy0(ww219, ww220, ww221, ww222, ww223, ww2240, ww2250)
new_deleteBy06(ww310, ww311, ww312, Succ(ww3130), Zero) → new_deleteBy(:%(Pos(Zero), Pos(Succ(ww312))), ww310)
new_deleteBy(:%(Neg(Zero), Neg(Zero)), :(:%(Pos(Zero), Pos(Succ(ww40100))), ww41)) → new_deleteBy(:%(Neg(Zero), Neg(Zero)), ww41)
new_deleteBy(:%(Pos(Succ(ww3000)), ww31), :(:%(Pos(Zero), ww401), ww41)) → new_deleteBy(:%(Pos(Succ(ww3000)), ww31), ww41)
new_deleteBy03(ww420, ww421, ww422, ww423, ww424, Succ(ww4250), Zero) → new_deleteBy02(ww420, ww421, Neg(Succ(ww422)), ww423, Neg(Succ(ww424)))
new_deleteBy03(ww420, ww421, ww422, ww423, ww424, Zero, Succ(ww4260)) → new_deleteBy02(ww420, ww421, Neg(Succ(ww422)), ww423, Neg(Succ(ww424)))
new_deleteBy0(ww219, ww220, ww221, ww222, ww223, Zero, Succ(ww2250)) → new_deleteBy00(ww219, ww220, ww221, ww222, ww223)
new_deleteBy019(ww227, ww228, ww229, ww230, ww231) → new_deleteBy(:%(Neg(Succ(ww230)), ww231), ww227)
new_deleteBy08(ww227, ww228, Pos(Zero), ww230, Pos(Succ(ww23100)), Zero, Zero) → new_deleteBy019(ww227, ww228, Pos(Zero), ww230, Pos(Succ(ww23100)))
new_deleteBy0(ww219, ww220, Neg(Succ(ww22100)), ww222, Neg(Succ(ww22300)), Zero, Zero) → new_deleteBy03(ww219, ww220, ww22100, ww222, ww22300, ww22300, ww22100)
new_deleteBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Pos(Zero), Pos(Succ(ww40100))), ww41)) → new_deleteBy09(ww41, ww40100, ww3100, ww3100, ww40100)
new_deleteBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Zero), Pos(Zero)), ww41)) → new_deleteBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_deleteBy08(ww227, ww228, Neg(Succ(ww22900)), ww230, Neg(Succ(ww23100)), Zero, Zero) → new_deleteBy020(ww227, ww228, ww22900, ww230, ww23100, ww23100, ww22900)
new_deleteBy05(ww304, ww305, ww306, Succ(ww3070), Succ(ww3080)) → new_deleteBy05(ww304, ww305, ww306, ww3070, ww3080)
new_deleteBy(:%(Pos(Zero), ww31), :(:%(Pos(Succ(ww40000)), ww401), ww41)) → new_deleteBy(:%(Pos(Zero), ww31), ww41)
new_deleteBy(:%(Neg(Zero), Pos(Zero)), :(:%(Neg(Zero), Neg(Succ(ww40100))), ww41)) → new_deleteBy(:%(Neg(Zero), Pos(Zero)), ww41)
new_deleteBy(:%(Pos(Zero), Neg(Zero)), :(:%(Neg(Zero), Neg(Succ(ww40100))), ww41)) → new_deleteBy(:%(Pos(Zero), Neg(Zero)), ww41)
new_deleteBy08(ww227, ww228, Pos(Succ(ww22900)), ww230, Pos(Succ(ww23100)), Zero, Zero) → new_deleteBy018(ww227, ww228, ww22900, ww230, ww23100, ww23100, ww22900)
new_deleteBy011(ww334, ww335, ww336, Succ(ww3370), Succ(ww3380)) → new_deleteBy011(ww334, ww335, ww336, ww3370, ww3380)
new_deleteBy04(ww298, ww299, ww300, Zero, Succ(ww3020)) → new_deleteBy013(ww298, ww299, ww300)
new_deleteBy0(ww219, ww220, Neg(Succ(ww22100)), ww222, Pos(Zero), Zero, Zero) → new_deleteBy02(ww219, ww220, Neg(Succ(ww22100)), ww222, Pos(Zero))
new_deleteBy0(ww219, ww220, Pos(Succ(ww22100)), ww222, Neg(Zero), Zero, Zero) → new_deleteBy02(ww219, ww220, Pos(Succ(ww22100)), ww222, Neg(Zero))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 4 SCCs.

↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
QDP
                        ↳ QDPSizeChangeProof
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_deleteBy03(ww420, ww421, ww422, ww423, ww424, Succ(ww4250), Zero) → new_deleteBy02(ww420, ww421, Neg(Succ(ww422)), ww423, Neg(Succ(ww424)))
new_deleteBy03(ww420, ww421, ww422, ww423, ww424, Zero, Succ(ww4260)) → new_deleteBy02(ww420, ww421, Neg(Succ(ww422)), ww423, Neg(Succ(ww424)))
new_deleteBy(:%(Pos(Succ(ww3000)), ww31), :(:%(Pos(Zero), ww401), ww41)) → new_deleteBy(:%(Pos(Succ(ww3000)), ww31), ww41)
new_deleteBy0(ww219, ww220, Pos(Succ(ww22100)), ww222, Pos(Succ(ww22300)), Zero, Zero) → new_deleteBy01(ww219, ww220, ww22100, ww222, ww22300, ww22300, ww22100)
new_deleteBy0(ww219, ww220, ww221, ww222, ww223, Zero, Succ(ww2250)) → new_deleteBy00(ww219, ww220, ww221, ww222, ww223)
new_deleteBy0(ww219, ww220, Neg(Succ(ww22100)), ww222, Neg(Zero), Zero, Zero) → new_deleteBy02(ww219, ww220, Neg(Succ(ww22100)), ww222, Neg(Zero))
new_deleteBy0(ww219, ww220, Neg(Zero), ww222, Neg(Succ(ww22300)), Zero, Zero) → new_deleteBy02(ww219, ww220, Neg(Zero), ww222, Neg(Succ(ww22300)))
new_deleteBy(:%(Pos(Succ(ww3000)), ww31), :(:%(Neg(ww4000), ww401), ww41)) → new_deleteBy(:%(Pos(Succ(ww3000)), ww31), ww41)
new_deleteBy0(ww219, ww220, Pos(ww2210), ww222, Neg(Succ(ww22300)), Zero, Zero) → new_deleteBy02(ww219, ww220, Pos(ww2210), ww222, Neg(Succ(ww22300)))
new_deleteBy0(ww219, ww220, Neg(ww2210), ww222, Pos(Succ(ww22300)), Zero, Zero) → new_deleteBy02(ww219, ww220, Neg(ww2210), ww222, Pos(Succ(ww22300)))
new_deleteBy0(ww219, ww220, Neg(Succ(ww22100)), ww222, Neg(Succ(ww22300)), Zero, Zero) → new_deleteBy03(ww219, ww220, ww22100, ww222, ww22300, ww22300, ww22100)
new_deleteBy03(ww420, ww421, ww422, ww423, ww424, Succ(ww4250), Succ(ww4260)) → new_deleteBy03(ww420, ww421, ww422, ww423, ww424, ww4250, ww4260)
new_deleteBy01(ww412, ww413, ww414, ww415, ww416, Succ(ww4170), Succ(ww4180)) → new_deleteBy01(ww412, ww413, ww414, ww415, ww416, ww4170, ww4180)
new_deleteBy00(ww219, ww220, ww221, ww222, ww223) → new_deleteBy(:%(Pos(Succ(ww222)), ww223), ww219)
new_deleteBy(:%(Pos(Succ(ww3000)), ww31), :(:%(Pos(Succ(ww40000)), ww401), ww41)) → new_deleteBy0(ww41, ww40000, ww401, ww3000, ww31, ww3000, ww40000)
new_deleteBy0(ww219, ww220, ww221, ww222, ww223, Succ(ww2240), Succ(ww2250)) → new_deleteBy0(ww219, ww220, ww221, ww222, ww223, ww2240, ww2250)
new_deleteBy0(ww219, ww220, ww221, ww222, ww223, Succ(ww2240), Zero) → new_deleteBy(:%(Pos(Succ(ww222)), ww223), ww219)
new_deleteBy0(ww219, ww220, Pos(Succ(ww22100)), ww222, Pos(Zero), Zero, Zero) → new_deleteBy02(ww219, ww220, Pos(Succ(ww22100)), ww222, Pos(Zero))
new_deleteBy01(ww412, ww413, ww414, ww415, ww416, Zero, Succ(ww4180)) → new_deleteBy02(ww412, ww413, Pos(Succ(ww414)), ww415, Pos(Succ(ww416)))
new_deleteBy01(ww412, ww413, ww414, ww415, ww416, Succ(ww4170), Zero) → new_deleteBy02(ww412, ww413, Pos(Succ(ww414)), ww415, Pos(Succ(ww416)))
new_deleteBy0(ww219, ww220, Pos(Zero), ww222, Pos(Succ(ww22300)), Zero, Zero) → new_deleteBy02(ww219, ww220, Pos(Zero), ww222, Pos(Succ(ww22300)))
new_deleteBy0(ww219, ww220, Neg(Succ(ww22100)), ww222, Pos(Zero), Zero, Zero) → new_deleteBy02(ww219, ww220, Neg(Succ(ww22100)), ww222, Pos(Zero))
new_deleteBy0(ww219, ww220, Pos(Succ(ww22100)), ww222, Neg(Zero), Zero, Zero) → new_deleteBy02(ww219, ww220, Pos(Succ(ww22100)), ww222, Neg(Zero))
new_deleteBy02(ww219, ww220, ww221, ww222, ww223) → new_deleteBy(:%(Pos(Succ(ww222)), ww223), ww219)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
QDP
                        ↳ QDPSizeChangeProof
                      ↳ QDP
                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_deleteBy022(ww328, ww329, ww330) → new_deleteBy(:%(Neg(Zero), Neg(Succ(ww330))), ww328)
new_deleteBy010(ww328, ww329, ww330, Succ(ww3310), Zero) → new_deleteBy(:%(Neg(Zero), Neg(Succ(ww330))), ww328)
new_deleteBy011(ww334, ww335, ww336, Succ(ww3370), Zero) → new_deleteBy(:%(Neg(Zero), Pos(Succ(ww336))), ww334)
new_deleteBy023(ww334, ww335, ww336) → new_deleteBy(:%(Neg(Zero), Pos(Succ(ww336))), ww334)
new_deleteBy09(ww322, ww323, ww324, Succ(ww3250), Succ(ww3260)) → new_deleteBy09(ww322, ww323, ww324, ww3250, ww3260)
new_deleteBy012(ww340, ww341, ww342, Succ(ww3430), Succ(ww3440)) → new_deleteBy012(ww340, ww341, ww342, ww3430, ww3440)
new_deleteBy010(ww328, ww329, ww330, Succ(ww3310), Succ(ww3320)) → new_deleteBy010(ww328, ww329, ww330, ww3310, ww3320)
new_deleteBy024(ww340, ww341, ww342) → new_deleteBy(:%(Neg(Zero), Neg(Succ(ww342))), ww340)
new_deleteBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Zero), Pos(Succ(ww40100))), ww41)) → new_deleteBy011(ww41, ww40100, ww3100, ww3100, ww40100)
new_deleteBy012(ww340, ww341, ww342, Zero, Succ(ww3440)) → new_deleteBy024(ww340, ww341, ww342)
new_deleteBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Zero), Pos(ww4010)), ww41)) → new_deleteBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_deleteBy09(ww322, ww323, ww324, Zero, Succ(ww3260)) → new_deleteBy021(ww322, ww323, ww324)
new_deleteBy(:%(Neg(Zero), ww31), :(:%(Neg(Succ(ww40000)), ww401), ww41)) → new_deleteBy(:%(Neg(Zero), ww31), ww41)
new_deleteBy010(ww328, ww329, ww330, Zero, Succ(ww3320)) → new_deleteBy022(ww328, ww329, ww330)
new_deleteBy09(ww322, ww323, ww324, Succ(ww3250), Zero) → new_deleteBy(:%(Neg(Zero), Pos(Succ(ww324))), ww322)
new_deleteBy011(ww334, ww335, ww336, Zero, Succ(ww3380)) → new_deleteBy023(ww334, ww335, ww336)
new_deleteBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Zero), Neg(Zero)), ww41)) → new_deleteBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_deleteBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Pos(Zero), Neg(ww4010)), ww41)) → new_deleteBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_deleteBy(:%(Neg(Zero), Neg(Zero)), :(:%(Pos(Zero), Pos(Succ(ww40100))), ww41)) → new_deleteBy(:%(Neg(Zero), Neg(Zero)), ww41)
new_deleteBy(:%(Neg(Zero), Neg(Zero)), :(:%(Neg(Zero), Pos(Succ(ww40100))), ww41)) → new_deleteBy(:%(Neg(Zero), Neg(Zero)), ww41)
new_deleteBy(:%(Neg(Zero), Neg(Zero)), :(:%(Pos(Zero), Neg(Succ(ww40100))), ww41)) → new_deleteBy(:%(Neg(Zero), Neg(Zero)), ww41)
new_deleteBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Neg(Zero), Neg(Zero)), ww41)) → new_deleteBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_deleteBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Zero), Neg(ww4010)), ww41)) → new_deleteBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_deleteBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Zero), Neg(Succ(ww40100))), ww41)) → new_deleteBy010(ww41, ww40100, ww3100, ww3100, ww40100)
new_deleteBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Neg(Zero), Neg(Succ(ww40100))), ww41)) → new_deleteBy012(ww41, ww40100, ww3100, ww3100, ww40100)
new_deleteBy(:%(Neg(Zero), ww31), :(:%(Pos(Succ(ww40000)), ww401), ww41)) → new_deleteBy(:%(Neg(Zero), ww31), ww41)
new_deleteBy(:%(Neg(Zero), Pos(Zero)), :(:%(Pos(Zero), Neg(Succ(ww40100))), ww41)) → new_deleteBy(:%(Neg(Zero), Pos(Zero)), ww41)
new_deleteBy(:%(Neg(Zero), Pos(Zero)), :(:%(Neg(Zero), Pos(Succ(ww40100))), ww41)) → new_deleteBy(:%(Neg(Zero), Pos(Zero)), ww41)
new_deleteBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Neg(Zero), Pos(ww4010)), ww41)) → new_deleteBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_deleteBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Zero), Pos(Zero)), ww41)) → new_deleteBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_deleteBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Pos(Zero), Pos(Succ(ww40100))), ww41)) → new_deleteBy09(ww41, ww40100, ww3100, ww3100, ww40100)
new_deleteBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Pos(Zero), Pos(Zero)), ww41)) → new_deleteBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_deleteBy(:%(Neg(Zero), Neg(Zero)), :(:%(Neg(Zero), Neg(Succ(ww40100))), ww41)) → new_deleteBy(:%(Neg(Zero), Neg(Zero)), ww41)
new_deleteBy021(ww322, ww323, ww324) → new_deleteBy(:%(Neg(Zero), Pos(Succ(ww324))), ww322)
new_deleteBy(:%(Neg(Zero), Pos(Zero)), :(:%(Neg(Zero), Neg(Succ(ww40100))), ww41)) → new_deleteBy(:%(Neg(Zero), Pos(Zero)), ww41)
new_deleteBy011(ww334, ww335, ww336, Succ(ww3370), Succ(ww3380)) → new_deleteBy011(ww334, ww335, ww336, ww3370, ww3380)
new_deleteBy(:%(Neg(Zero), Pos(Zero)), :(:%(Pos(Zero), Pos(Succ(ww40100))), ww41)) → new_deleteBy(:%(Neg(Zero), Pos(Zero)), ww41)
new_deleteBy012(ww340, ww341, ww342, Succ(ww3430), Zero) → new_deleteBy(:%(Neg(Zero), Neg(Succ(ww342))), ww340)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
QDP
                        ↳ QDPSizeChangeProof
                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_deleteBy08(ww227, ww228, Neg(Succ(ww22900)), ww230, Pos(Zero), Zero, Zero) → new_deleteBy019(ww227, ww228, Neg(Succ(ww22900)), ww230, Pos(Zero))
new_deleteBy08(ww227, ww228, Pos(Succ(ww22900)), ww230, Neg(Zero), Zero, Zero) → new_deleteBy019(ww227, ww228, Pos(Succ(ww22900)), ww230, Neg(Zero))
new_deleteBy020(ww436, ww437, ww438, ww439, ww440, Succ(ww4410), Succ(ww4420)) → new_deleteBy020(ww436, ww437, ww438, ww439, ww440, ww4410, ww4420)
new_deleteBy08(ww227, ww228, Pos(Zero), ww230, Pos(Succ(ww23100)), Zero, Zero) → new_deleteBy019(ww227, ww228, Pos(Zero), ww230, Pos(Succ(ww23100)))
new_deleteBy019(ww227, ww228, ww229, ww230, ww231) → new_deleteBy(:%(Neg(Succ(ww230)), ww231), ww227)
new_deleteBy(:%(Neg(Succ(ww3000)), ww31), :(:%(Neg(Succ(ww40000)), ww401), ww41)) → new_deleteBy08(ww41, ww40000, ww401, ww3000, ww31, ww3000, ww40000)
new_deleteBy08(ww227, ww228, Neg(Succ(ww22900)), ww230, Neg(Zero), Zero, Zero) → new_deleteBy019(ww227, ww228, Neg(Succ(ww22900)), ww230, Neg(Zero))
new_deleteBy020(ww436, ww437, ww438, ww439, ww440, Succ(ww4410), Zero) → new_deleteBy019(ww436, ww437, Neg(Succ(ww438)), ww439, Neg(Succ(ww440)))
new_deleteBy020(ww436, ww437, ww438, ww439, ww440, Zero, Succ(ww4420)) → new_deleteBy019(ww436, ww437, Neg(Succ(ww438)), ww439, Neg(Succ(ww440)))
new_deleteBy08(ww227, ww228, ww229, ww230, ww231, Succ(ww2320), Succ(ww2330)) → new_deleteBy08(ww227, ww228, ww229, ww230, ww231, ww2320, ww2330)
new_deleteBy08(ww227, ww228, Pos(Succ(ww22900)), ww230, Pos(Zero), Zero, Zero) → new_deleteBy019(ww227, ww228, Pos(Succ(ww22900)), ww230, Pos(Zero))
new_deleteBy(:%(Neg(Succ(ww3000)), ww31), :(:%(Neg(Zero), ww401), ww41)) → new_deleteBy(:%(Neg(Succ(ww3000)), ww31), ww41)
new_deleteBy018(ww428, ww429, ww430, ww431, ww432, Succ(ww4330), Zero) → new_deleteBy019(ww428, ww429, Pos(Succ(ww430)), ww431, Pos(Succ(ww432)))
new_deleteBy018(ww428, ww429, ww430, ww431, ww432, Zero, Succ(ww4340)) → new_deleteBy019(ww428, ww429, Pos(Succ(ww430)), ww431, Pos(Succ(ww432)))
new_deleteBy08(ww227, ww228, Neg(Zero), ww230, Neg(Succ(ww23100)), Zero, Zero) → new_deleteBy019(ww227, ww228, Neg(Zero), ww230, Neg(Succ(ww23100)))
new_deleteBy08(ww227, ww228, ww229, ww230, ww231, Zero, Succ(ww2330)) → new_deleteBy017(ww227, ww228, ww229, ww230, ww231)
new_deleteBy08(ww227, ww228, Neg(Succ(ww22900)), ww230, Neg(Succ(ww23100)), Zero, Zero) → new_deleteBy020(ww227, ww228, ww22900, ww230, ww23100, ww23100, ww22900)
new_deleteBy018(ww428, ww429, ww430, ww431, ww432, Succ(ww4330), Succ(ww4340)) → new_deleteBy018(ww428, ww429, ww430, ww431, ww432, ww4330, ww4340)
new_deleteBy08(ww227, ww228, Pos(Succ(ww22900)), ww230, Pos(Succ(ww23100)), Zero, Zero) → new_deleteBy018(ww227, ww228, ww22900, ww230, ww23100, ww23100, ww22900)
new_deleteBy08(ww227, ww228, Pos(ww2290), ww230, Neg(Succ(ww23100)), Zero, Zero) → new_deleteBy019(ww227, ww228, Pos(ww2290), ww230, Neg(Succ(ww23100)))
new_deleteBy08(ww227, ww228, Neg(ww2290), ww230, Pos(Succ(ww23100)), Zero, Zero) → new_deleteBy019(ww227, ww228, Neg(ww2290), ww230, Pos(Succ(ww23100)))
new_deleteBy(:%(Neg(Succ(ww3000)), ww31), :(:%(Pos(ww4000), ww401), ww41)) → new_deleteBy(:%(Neg(Succ(ww3000)), ww31), ww41)
new_deleteBy017(ww227, ww228, ww229, ww230, ww231) → new_deleteBy(:%(Neg(Succ(ww230)), ww231), ww227)
new_deleteBy08(ww227, ww228, ww229, ww230, ww231, Succ(ww2320), Zero) → new_deleteBy(:%(Neg(Succ(ww230)), ww231), ww227)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
QDP
                        ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_deleteBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Zero), Neg(Succ(ww40100))), ww41)) → new_deleteBy05(ww41, ww40100, ww3100, ww3100, ww40100)
new_deleteBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Zero), Neg(ww4010)), ww41)) → new_deleteBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_deleteBy015(ww310, ww311, ww312) → new_deleteBy(:%(Pos(Zero), Pos(Succ(ww312))), ww310)
new_deleteBy04(ww298, ww299, ww300, Succ(ww3010), Succ(ww3020)) → new_deleteBy04(ww298, ww299, ww300, ww3010, ww3020)
new_deleteBy016(ww316, ww317, ww318) → new_deleteBy(:%(Pos(Zero), Neg(Succ(ww318))), ww316)
new_deleteBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Zero), Pos(Succ(ww40100))), ww41)) → new_deleteBy06(ww41, ww40100, ww3100, ww3100, ww40100)
new_deleteBy07(ww316, ww317, ww318, Zero, Succ(ww3200)) → new_deleteBy016(ww316, ww317, ww318)
new_deleteBy(:%(Pos(Zero), Pos(Zero)), :(:%(Pos(Zero), Pos(Succ(ww40100))), ww41)) → new_deleteBy(:%(Pos(Zero), Pos(Zero)), ww41)
new_deleteBy05(ww304, ww305, ww306, Zero, Succ(ww3080)) → new_deleteBy014(ww304, ww305, ww306)
new_deleteBy06(ww310, ww311, ww312, Zero, Succ(ww3140)) → new_deleteBy015(ww310, ww311, ww312)
new_deleteBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Zero), Pos(ww4010)), ww41)) → new_deleteBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_deleteBy013(ww298, ww299, ww300) → new_deleteBy(:%(Pos(Zero), Pos(Succ(ww300))), ww298)
new_deleteBy05(ww304, ww305, ww306, Succ(ww3070), Zero) → new_deleteBy(:%(Pos(Zero), Neg(Succ(ww306))), ww304)
new_deleteBy06(ww310, ww311, ww312, Succ(ww3130), Zero) → new_deleteBy(:%(Pos(Zero), Pos(Succ(ww312))), ww310)
new_deleteBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Neg(Zero), Pos(ww4010)), ww41)) → new_deleteBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_deleteBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Pos(Zero), Pos(Succ(ww40100))), ww41)) → new_deleteBy04(ww41, ww40100, ww3100, ww3100, ww40100)
new_deleteBy(:%(Pos(Zero), Pos(Zero)), :(:%(Neg(Zero), Neg(Succ(ww40100))), ww41)) → new_deleteBy(:%(Pos(Zero), Pos(Zero)), ww41)
new_deleteBy04(ww298, ww299, ww300, Succ(ww3010), Zero) → new_deleteBy(:%(Pos(Zero), Pos(Succ(ww300))), ww298)
new_deleteBy014(ww304, ww305, ww306) → new_deleteBy(:%(Pos(Zero), Neg(Succ(ww306))), ww304)
new_deleteBy06(ww310, ww311, ww312, Succ(ww3130), Succ(ww3140)) → new_deleteBy06(ww310, ww311, ww312, ww3130, ww3140)
new_deleteBy(:%(Pos(Zero), Neg(Zero)), :(:%(Neg(Zero), Pos(Succ(ww40100))), ww41)) → new_deleteBy(:%(Pos(Zero), Neg(Zero)), ww41)
new_deleteBy(:%(Pos(Zero), Neg(Zero)), :(:%(Pos(Zero), Neg(Succ(ww40100))), ww41)) → new_deleteBy(:%(Pos(Zero), Neg(Zero)), ww41)
new_deleteBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Zero), Neg(Zero)), ww41)) → new_deleteBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_deleteBy07(ww316, ww317, ww318, Succ(ww3190), Zero) → new_deleteBy(:%(Pos(Zero), Neg(Succ(ww318))), ww316)
new_deleteBy(:%(Pos(Zero), Pos(Zero)), :(:%(Pos(Zero), Neg(Succ(ww40100))), ww41)) → new_deleteBy(:%(Pos(Zero), Pos(Zero)), ww41)
new_deleteBy(:%(Pos(Zero), Pos(Zero)), :(:%(Neg(Zero), Pos(Succ(ww40100))), ww41)) → new_deleteBy(:%(Pos(Zero), Pos(Zero)), ww41)
new_deleteBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Pos(Zero), Pos(Zero)), ww41)) → new_deleteBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_deleteBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Neg(Zero), Neg(Succ(ww40100))), ww41)) → new_deleteBy07(ww41, ww40100, ww3100, ww3100, ww40100)
new_deleteBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Zero), Pos(Zero)), ww41)) → new_deleteBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_deleteBy05(ww304, ww305, ww306, Succ(ww3070), Succ(ww3080)) → new_deleteBy05(ww304, ww305, ww306, ww3070, ww3080)
new_deleteBy07(ww316, ww317, ww318, Succ(ww3190), Succ(ww3200)) → new_deleteBy07(ww316, ww317, ww318, ww3190, ww3200)
new_deleteBy(:%(Pos(Zero), ww31), :(:%(Neg(Succ(ww40000)), ww401), ww41)) → new_deleteBy(:%(Pos(Zero), ww31), ww41)
new_deleteBy(:%(Pos(Zero), ww31), :(:%(Pos(Succ(ww40000)), ww401), ww41)) → new_deleteBy(:%(Pos(Zero), ww31), ww41)
new_deleteBy(:%(Pos(Zero), Neg(Zero)), :(:%(Neg(Zero), Neg(Succ(ww40100))), ww41)) → new_deleteBy(:%(Pos(Zero), Neg(Zero)), ww41)
new_deleteBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Neg(Zero), Neg(Zero)), ww41)) → new_deleteBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_deleteBy(:%(Pos(Zero), Neg(Zero)), :(:%(Pos(Zero), Pos(Succ(ww40100))), ww41)) → new_deleteBy(:%(Pos(Zero), Neg(Zero)), ww41)
new_deleteBy04(ww298, ww299, ww300, Zero, Succ(ww3020)) → new_deleteBy013(ww298, ww299, ww300)
new_deleteBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Pos(Zero), Neg(ww4010)), ww41)) → new_deleteBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: